Report for Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/transmitter.06_false-unreach-call_false-termination.cil/transmitter.06_false-unreach-call_false-termination.cil.c (Counterexample 1)

Generated on 2025-08-28 17:17:33 by CPAchecker 4.0 / terminationAnalysis

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
extern void __VERIFIER_error() __attribute__ ((__noreturn__));  
2
  
3
extern int __VERIFIER_nondet_int();  
4
/* Generated by CIL v. 1.3.6 */  
5
/* print_CIL_Input is true */  
6
  
7
void error(void)   
8
{   
9
  
10
  {  
11
  ERROR: __VERIFIER_error();  
12
  return;  
13
}  
14
}  
15
int m_pc  =    0;  
16
int t1_pc  =    0;  
17
int t2_pc  =    0;  
18
int t3_pc  =    0;  
19
int t4_pc  =    0;  
20
int t5_pc  =    0;  
21
int t6_pc  =    0;  
22
int m_st  ;  
23
int t1_st  ;  
24
int t2_st  ;  
25
int t3_st  ;  
26
int t4_st  ;  
27
int t5_st  ;  
28
int t6_st  ;  
29
int m_i  ;  
30
int t1_i  ;  
31
int t2_i  ;  
32
int t3_i  ;  
33
int t4_i  ;  
34
int t5_i  ;  
35
int t6_i  ;  
36
int M_E  =    2;  
37
int T1_E  =    2;  
38
int T2_E  =    2;  
39
int T3_E  =    2;  
40
int T4_E  =    2;  
41
int T5_E  =    2;  
42
int T6_E  =    2;  
43
int E_1  =    2;  
44
int E_2  =    2;  
45
int E_3  =    2;  
46
int E_4  =    2;  
47
int E_5  =    2;  
48
int E_6  =    2;  
49
int is_master_triggered(void) ;  
50
int is_transmit1_triggered(void) ;  
51
int is_transmit2_triggered(void) ;  
52
int is_transmit3_triggered(void) ;  
53
int is_transmit4_triggered(void) ;  
54
int is_transmit5_triggered(void) ;  
55
int is_transmit6_triggered(void) ;  
56
void immediate_notify(void) ;  
57
void master(void)   
58
{   
59
  
60
  {  
61
  if (m_pc == 0) {  
62
    goto M_ENTRY;  
63
  } else {  
64
    if (m_pc == 1) {  
65
      goto M_WAIT;  
66
    } else {  
67
  
68
    }  
69
  }  
70
  M_ENTRY: ;  
71
  {  
72
  while (1) {  
73
    while_0_continue: /* CIL Label */ ;  
74
    {  
75
    E_1 = 1;  
76
    immediate_notify();  
77
    E_1 = 2;  
78
    }  
79
    {  
80
    while (1) {  
81
      while_1_continue: /* CIL Label */ ;  
82
      m_pc = 1;  
83
      m_st = 2;  
84
  
85
      goto return_label;  
86
      M_WAIT: ;  
87
    }  
88
    while_1_break: /* CIL Label */ ;  
89
    }  
90
  }  
91
  while_0_break: /* CIL Label */ ;  
92
  }  
93
  
94
  return_label: /* CIL Label */   
95
  return;  
96
}  
97
}  
98
void transmit1(void)   
99
{   
100
  
101
  {  
102
  if (t1_pc == 0) {  
103
    goto T1_ENTRY;  
104
  } else {  
105
    if (t1_pc == 1) {  
106
      goto T1_WAIT;  
107
    } else {  
108
  
109
    }  
110
  }  
111
  T1_ENTRY: ;  
112
  {  
113
  while (1) {  
114
    while_2_continue: /* CIL Label */ ;  
115
    t1_pc = 1;  
116
    t1_st = 2;  
117
  
118
    goto return_label;  
119
    T1_WAIT:   
120
    {  
121
    E_2 = 1;  
122
    immediate_notify();  
123
    E_2 = 2;  
124
    }  
125
  }  
126
  while_2_break: /* CIL Label */ ;  
127
  }  
128
  
129
  return_label: /* CIL Label */   
130
  return;  
131
}  
132
}  
133
void transmit2(void)   
134
{   
135
  
136
  {  
137
  if (t2_pc == 0) {  
138
    goto T2_ENTRY;  
139
  } else {  
140
    if (t2_pc == 1) {  
141
      goto T2_WAIT;  
142
    } else {  
143
  
144
    }  
145
  }  
146
  T2_ENTRY: ;  
147
  {  
148
  while (1) {  
149
    while_3_continue: /* CIL Label */ ;  
150
    t2_pc = 1;  
151
    t2_st = 2;  
152
  
153
    goto return_label;  
154
    T2_WAIT:   
155
    {  
156
    E_3 = 1;  
157
    immediate_notify();  
158
    E_3 = 2;  
159
    }  
160
  }  
161
  while_3_break: /* CIL Label */ ;  
162
  }  
163
  
164
  return_label: /* CIL Label */   
165
  return;  
166
}  
167
}  
168
void transmit3(void)   
169
{   
170
  
171
  {  
172
  if (t3_pc == 0) {  
173
    goto T3_ENTRY;  
174
  } else {  
175
    if (t3_pc == 1) {  
176
      goto T3_WAIT;  
177
    } else {  
178
  
179
    }  
180
  }  
181
  T3_ENTRY: ;  
182
  {  
183
  while (1) {  
184
    while_4_continue: /* CIL Label */ ;  
185
    t3_pc = 1;  
186
    t3_st = 2;  
187
  
188
    goto return_label;  
189
    T3_WAIT:   
190
    {  
191
    E_4 = 1;  
192
    immediate_notify();  
193
    E_4 = 2;  
194
    }  
195
  }  
196
  while_4_break: /* CIL Label */ ;  
197
  }  
198
  
199
  return_label: /* CIL Label */   
200
  return;  
201
}  
202
}  
203
void transmit4(void)   
204
{   
205
  
206
  {  
207
  if (t4_pc == 0) {  
208
    goto T4_ENTRY;  
209
  } else {  
210
    if (t4_pc == 1) {  
211
      goto T4_WAIT;  
212
    } else {  
213
  
214
    }  
215
  }  
216
  T4_ENTRY: ;  
217
  {  
218
  while (1) {  
219
    while_5_continue: /* CIL Label */ ;  
220
    t4_pc = 1;  
221
    t4_st = 2;  
222
  
223
    goto return_label;  
224
    T4_WAIT:   
225
    {  
226
    E_5 = 1;  
227
    immediate_notify();  
228
    E_5 = 2;  
229
    }  
230
  }  
231
  while_5_break: /* CIL Label */ ;  
232
  }  
233
  
234
  return_label: /* CIL Label */   
235
  return;  
236
}  
237
}  
238
void transmit5(void)   
239
{   
240
  
241
  {  
242
  if (t5_pc == 0) {  
243
    goto T5_ENTRY;  
244
  } else {  
245
    if (t5_pc == 1) {  
246
      goto T5_WAIT;  
247
    } else {  
248
  
249
    }  
250
  }  
251
  T5_ENTRY: ;  
252
  {  
253
  while (1) {  
254
    while_6_continue: /* CIL Label */ ;  
255
    t5_pc = 1;  
256
    t5_st = 2;  
257
  
258
    goto return_label;  
259
    T5_WAIT:   
260
    {  
261
    E_6 = 1;  
262
    immediate_notify();  
263
    E_6 = 2;  
264
    }  
265
  }  
266
  while_6_break: /* CIL Label */ ;  
267
  }  
268
  
269
  return_label: /* CIL Label */   
270
  return;  
271
}  
272
}  
273
void transmit6(void)   
274
{   
275
  
276
  {  
277
  if (t6_pc == 0) {  
278
    goto T6_ENTRY;  
279
  } else {  
280
    if (t6_pc == 1) {  
281
      goto T6_WAIT;  
282
    } else {  
283
  
284
    }  
285
  }  
286
  T6_ENTRY: ;  
287
  {  
288
  while (1) {  
289
    while_7_continue: /* CIL Label */ ;  
290
    t6_pc = 1;  
291
    t6_st = 2;  
292
  
293
    goto return_label;  
294
    T6_WAIT:   
295
    {  
296
    error();  
297
    }  
298
  }  
299
  while_7_break: /* CIL Label */ ;  
300
  }  
301
  
302
  return_label: /* CIL Label */   
303
  return;  
304
}  
305
}  
306
int is_master_triggered(void)   
307
{ int __retres1 ;  
308
  
309
  {  
310
  if (m_pc == 1) {  
311
    if (M_E == 1) {  
312
      __retres1 = 1;  
313
      goto return_label;  
314
    } else {  
315
  
316
    }  
317
  } else {  
318
  
319
  }  
320
  __retres1 = 0;  
321
  return_label: /* CIL Label */   
322
  return (__retres1);  
323
}  
324
}  
325
int is_transmit1_triggered(void)   
326
{ int __retres1 ;  
327
  
328
  {  
329
  if (t1_pc == 1) {  
330
    if (E_1 == 1) {  
331
      __retres1 = 1;  
332
      goto return_label;  
333
    } else {  
334
  
335
    }  
336
  } else {  
337
  
338
  }  
339
  __retres1 = 0;  
340
  return_label: /* CIL Label */   
341
  return (__retres1);  
342
}  
343
}  
344
int is_transmit2_triggered(void)   
345
{ int __retres1 ;  
346
  
347
  {  
348
  if (t2_pc == 1) {  
349
    if (E_2 == 1) {  
350
      __retres1 = 1;  
351
      goto return_label;  
352
    } else {  
353
  
354
    }  
355
  } else {  
356
  
357
  }  
358
  __retres1 = 0;  
359
  return_label: /* CIL Label */   
360
  return (__retres1);  
361
}  
362
}  
363
int is_transmit3_triggered(void)   
364
{ int __retres1 ;  
365
  
366
  {  
367
  if (t3_pc == 1) {  
368
    if (E_3 == 1) {  
369
      __retres1 = 1;  
370
      goto return_label;  
371
    } else {  
372
  
373
    }  
374
  } else {  
375
  
376
  }  
377
  __retres1 = 0;  
378
  return_label: /* CIL Label */   
379
  return (__retres1);  
380
}  
381
}  
382
int is_transmit4_triggered(void)   
383
{ int __retres1 ;  
384
  
385
  {  
386
  if (t4_pc == 1) {  
387
    if (E_4 == 1) {  
388
      __retres1 = 1;  
389
      goto return_label;  
390
    } else {  
391
  
392
    }  
393
  } else {  
394
  
395
  }  
396
  __retres1 = 0;  
397
  return_label: /* CIL Label */   
398
  return (__retres1);  
399
}  
400
}  
401
int is_transmit5_triggered(void)   
402
{ int __retres1 ;  
403
  
404
  {  
405
  if (t5_pc == 1) {  
406
    if (E_5 == 1) {  
407
      __retres1 = 1;  
408
      goto return_label;  
409
    } else {  
410
  
411
    }  
412
  } else {  
413
  
414
  }  
415
  __retres1 = 0;  
416
  return_label: /* CIL Label */   
417
  return (__retres1);  
418
}  
419
}  
420
int is_transmit6_triggered(void)   
421
{ int __retres1 ;  
422
  
423
  {  
424
  if (t6_pc == 1) {  
425
    if (E_6 == 1) {  
426
      __retres1 = 1;  
427
      goto return_label;  
428
    } else {  
429
  
430
    }  
431
  } else {  
432
  
433
  }  
434
  __retres1 = 0;  
435
  return_label: /* CIL Label */   
436
  return (__retres1);  
437
}  
438
}  
439
void update_channels(void)   
440
{   
441
  
442
  {  
443
  
444
  return;  
445
}  
446
}  
447
void init_threads(void)   
448
{   
449
  
450
  {  
451
  if (m_i == 1) {  
452
    m_st = 0;  
453
  } else {  
454
    m_st = 2;  
455
  }  
456
  if (t1_i == 1) {  
457
    t1_st = 0;  
458
  } else {  
459
    t1_st = 2;  
460
  }  
461
  if (t2_i == 1) {  
462
    t2_st = 0;  
463
  } else {  
464
    t2_st = 2;  
465
  }  
466
  if (t3_i == 1) {  
467
    t3_st = 0;  
468
  } else {  
469
    t3_st = 2;  
470
  }  
471
  if (t4_i == 1) {  
472
    t4_st = 0;  
473
  } else {  
474
    t4_st = 2;  
475
  }  
476
  if (t5_i == 1) {  
477
    t5_st = 0;  
478
  } else {  
479
    t5_st = 2;  
480
  }  
481
  if (t6_i == 1) {  
482
    t6_st = 0;  
483
  } else {  
484
    t6_st = 2;  
485
  }  
486
  
487
  return;  
488
}  
489
}  
490
int exists_runnable_thread(void)   
491
{ int __retres1 ;  
492
  
493
  {  
494
  if (m_st == 0) {  
495
    __retres1 = 1;  
496
    goto return_label;  
497
  } else {  
498
    if (t1_st == 0) {  
499
      __retres1 = 1;  
500
      goto return_label;  
501
    } else {  
502
      if (t2_st == 0) {  
503
        __retres1 = 1;  
504
        goto return_label;  
505
      } else {  
506
        if (t3_st == 0) {  
507
          __retres1 = 1;  
508
          goto return_label;  
509
        } else {  
510
          if (t4_st == 0) {  
511
            __retres1 = 1;  
512
            goto return_label;  
513
          } else {  
514
            if (t5_st == 0) {  
515
              __retres1 = 1;  
516
              goto return_label;  
517
            } else {  
518
              if (t6_st == 0) {  
519
                __retres1 = 1;  
520
                goto return_label;  
521
              } else {  
522
  
523
              }  
524
            }  
525
          }  
526
        }  
527
      }  
528
    }  
529
  }  
530
  __retres1 = 0;  
531
  return_label: /* CIL Label */   
532
  return (__retres1);  
533
}  
534
}  
535
void eval(void)   
536
{  
537
  int tmp ;  
538
  
539
  {  
540
  {  
541
  while (1) {  
542
    while_8_continue: /* CIL Label */ ;  
543
    {  
544
    tmp = exists_runnable_thread();  
545
    }  
546
    if (tmp) {  
547
  
548
    } else {  
549
      goto while_8_break;  
550
    }  
551
    if (m_st == 0) {  
552
      int tmp_ndt_1;  
553
      tmp_ndt_1 = __VERIFIER_nondet_int();  
554
      if (tmp_ndt_1) {  
555
        {  
556
        m_st = 1;  
557
        master();  
558
        }  
559
      } else {  
560
  
561
      }  
562
    } else {  
563
  
564
    }  
565
    if (t1_st == 0) {  
566
      int tmp_ndt_2;  
567
      tmp_ndt_2 = __VERIFIER_nondet_int();  
568
      if (tmp_ndt_2) {  
569
        {  
570
        t1_st = 1;  
571
        transmit1();  
572
        }  
573
      } else {  
574
  
575
      }  
576
    } else {  
577
  
578
    }  
579
    if (t2_st == 0) {  
580
      int tmp_ndt_3;  
581
      tmp_ndt_3 = __VERIFIER_nondet_int();  
582
      if (tmp_ndt_3) {  
583
        {  
584
        t2_st = 1;  
585
        transmit2();  
586
        }  
587
      } else {  
588
  
589
      }  
590
    } else {  
591
  
592
    }  
593
    if (t3_st == 0) {  
594
      int tmp_ndt_4;  
595
      tmp_ndt_4 = __VERIFIER_nondet_int();  
596
      if (tmp_ndt_4) {  
597
        {  
598
        t3_st = 1;  
599
        transmit3();  
600
        }  
601
      } else {  
602
  
603
      }  
604
    } else {  
605
  
606
    }  
607
    if (t4_st == 0) {  
608
      int tmp_ndt_5;  
609
      tmp_ndt_5 = __VERIFIER_nondet_int();  
610
      if (tmp_ndt_5) {  
611
        {  
612
        t4_st = 1;  
613
        transmit4();  
614
        }  
615
      } else {  
616
  
617
      }  
618
    } else {  
619
  
620
    }  
621
    if (t5_st == 0) {  
622
      int tmp_ndt_6;  
623
      tmp_ndt_6 = __VERIFIER_nondet_int();  
624
      if (tmp_ndt_6) {  
625
        {  
626
        t5_st = 1;  
627
        transmit5();  
628
        }  
629
      } else {  
630
  
631
      }  
632
    } else {  
633
  
634
    }  
635
    if (t6_st == 0) {  
636
      int tmp_ndt_7;  
637
      tmp_ndt_7 = __VERIFIER_nondet_int();  
638
      if (tmp_ndt_7) {  
639
        {  
640
        t6_st = 1;  
641
        transmit6();  
642
        }  
643
      } else {  
644
  
645
      }  
646
    } else {  
647
  
648
    }  
649
  }  
650
  while_8_break: /* CIL Label */ ;  
651
  }  
652
  
653
  return;  
654
}  
655
}  
656
void fire_delta_events(void)   
657
{   
658
  
659
  {  
660
  if (M_E == 0) {  
661
    M_E = 1;  
662
  } else {  
663
  
664
  }  
665
  if (T1_E == 0) {  
666
    T1_E = 1;  
667
  } else {  
668
  
669
  }  
670
  if (T2_E == 0) {  
671
    T2_E = 1;  
672
  } else {  
673
  
674
  }  
675
  if (T3_E == 0) {  
676
    T3_E = 1;  
677
  } else {  
678
  
679
  }  
680
  if (T4_E == 0) {  
681
    T4_E = 1;  
682
  } else {  
683
  
684
  }  
685
  if (T5_E == 0) {  
686
    T5_E = 1;  
687
  } else {  
688
  
689
  }  
690
  if (T6_E == 0) {  
691
    T6_E = 1;  
692
  } else {  
693
  
694
  }  
695
  if (E_1 == 0) {  
696
    E_1 = 1;  
697
  } else {  
698
  
699
  }  
700
  if (E_2 == 0) {  
701
    E_2 = 1;  
702
  } else {  
703
  
704
  }  
705
  if (E_3 == 0) {  
706
    E_3 = 1;  
707
  } else {  
708
  
709
  }  
710
  if (E_4 == 0) {  
711
    E_4 = 1;  
712
  } else {  
713
  
714
  }  
715
  if (E_5 == 0) {  
716
    E_5 = 1;  
717
  } else {  
718
  
719
  }  
720
  if (E_6 == 0) {  
721
    E_6 = 1;  
722
  } else {  
723
  
724
  }  
725
  
726
  return;  
727
}  
728
}  
729
void reset_delta_events(void)   
730
{   
731
  
732
  {  
733
  if (M_E == 1) {  
734
    M_E = 2;  
735
  } else {  
736
  
737
  }  
738
  if (T1_E == 1) {  
739
    T1_E = 2;  
740
  } else {  
741
  
742
  }  
743
  if (T2_E == 1) {  
744
    T2_E = 2;  
745
  } else {  
746
  
747
  }  
748
  if (T3_E == 1) {  
749
    T3_E = 2;  
750
  } else {  
751
  
752
  }  
753
  if (T4_E == 1) {  
754
    T4_E = 2;  
755
  } else {  
756
  
757
  }  
758
  if (T5_E == 1) {  
759
    T5_E = 2;  
760
  } else {  
761
  
762
  }  
763
  if (T6_E == 1) {  
764
    T6_E = 2;  
765
  } else {  
766
  
767
  }  
768
  if (E_1 == 1) {  
769
    E_1 = 2;  
770
  } else {  
771
  
772
  }  
773
  if (E_2 == 1) {  
774
    E_2 = 2;  
775
  } else {  
776
  
777
  }  
778
  if (E_3 == 1) {  
779
    E_3 = 2;  
780
  } else {  
781
  
782
  }  
783
  if (E_4 == 1) {  
784
    E_4 = 2;  
785
  } else {  
786
  
787
  }  
788
  if (E_5 == 1) {  
789
    E_5 = 2;  
790
  } else {  
791
  
792
  }  
793
  if (E_6 == 1) {  
794
    E_6 = 2;  
795
  } else {  
796
  
797
  }  
798
  
799
  return;  
800
}  
801
}  
802
void activate_threads(void)   
803
{ int tmp ;  
804
  int tmp___0 ;  
805
  int tmp___1 ;  
806
  int tmp___2 ;  
807
  int tmp___3 ;  
808
  int tmp___4 ;  
809
  int tmp___5 ;  
810
  
811
  {  
812
  {  
813
  tmp = is_master_triggered();  
814
  }  
815
  if (tmp) {  
816
    m_st = 0;  
817
  } else {  
818
  
819
  }  
820
  {  
821
  tmp___0 = is_transmit1_triggered();  
822
  }  
823
  if (tmp___0) {  
824
    t1_st = 0;  
825
  } else {  
826
  
827
  }  
828
  {  
829
  tmp___1 = is_transmit2_triggered();  
830
  }  
831
  if (tmp___1) {  
832
    t2_st = 0;  
833
  } else {  
834
  
835
  }  
836
  {  
837
  tmp___2 = is_transmit3_triggered();  
838
  }  
839
  if (tmp___2) {  
840
    t3_st = 0;  
841
  } else {  
842
  
843
  }  
844
  {  
845
  tmp___3 = is_transmit4_triggered();  
846
  }  
847
  if (tmp___3) {  
848
    t4_st = 0;  
849
  } else {  
850
  
851
  }  
852
  {  
853
  tmp___4 = is_transmit5_triggered();  
854
  }  
855
  if (tmp___4) {  
856
    t5_st = 0;  
857
  } else {  
858
  
859
  }  
860
  {  
861
  tmp___5 = is_transmit6_triggered();  
862
  }  
863
  if (tmp___5) {  
864
    t6_st = 0;  
865
  } else {  
866
  
867
  }  
868
  
869
  return;  
870
}  
871
}  
872
void immediate_notify(void)   
873
{   
874
  
875
  {  
876
  {  
877
  activate_threads();  
878
  }  
879
  
880
  return;  
881
}  
882
}  
883
void fire_time_events(void)   
884
{   
885
  
886
  {  
887
  M_E = 1;  
888
  
889
  return;  
890
}  
891
}  
892
void reset_time_events(void)   
893
{   
894
  
895
  {  
896
  if (M_E == 1) {  
897
    M_E = 2;  
898
  } else {  
899
  
900
  }  
901
  if (T1_E == 1) {  
902
    T1_E = 2;  
903
  } else {  
904
  
905
  }  
906
  if (T2_E == 1) {  
907
    T2_E = 2;  
908
  } else {  
909
  
910
  }  
911
  if (T3_E == 1) {  
912
    T3_E = 2;  
913
  } else {  
914
  
915
  }  
916
  if (T4_E == 1) {  
917
    T4_E = 2;  
918
  } else {  
919
  
920
  }  
921
  if (T5_E == 1) {  
922
    T5_E = 2;  
923
  } else {  
924
  
925
  }  
926
  if (T6_E == 1) {  
927
    T6_E = 2;  
928
  } else {  
929
  
930
  }  
931
  if (E_1 == 1) {  
932
    E_1 = 2;  
933
  } else {  
934
  
935
  }  
936
  if (E_2 == 1) {  
937
    E_2 = 2;  
938
  } else {  
939
  
940
  }  
941
  if (E_3 == 1) {  
942
    E_3 = 2;  
943
  } else {  
944
  
945
  }  
946
  if (E_4 == 1) {  
947
    E_4 = 2;  
948
  } else {  
949
  
950
  }  
951
  if (E_5 == 1) {  
952
    E_5 = 2;  
953
  } else {  
954
  
955
  }  
956
  if (E_6 == 1) {  
957
    E_6 = 2;  
958
  } else {  
959
  
960
  }  
961
  
962
  return;  
963
}  
964
}  
965
void init_model(void)   
966
{   
967
  
968
  {  
969
  m_i = 1;  
970
  t1_i = 1;  
971
  t2_i = 1;  
972
  t3_i = 1;  
973
  t4_i = 1;  
974
  t5_i = 1;  
975
  t6_i = 1;  
976
  
977
  return;  
978
}  
979
}  
980
int stop_simulation(void)   
981
{ int tmp ;  
982
  int __retres2 ;  
983
  
984
  {  
985
  {  
986
  tmp = exists_runnable_thread();  
987
  }  
988
  if (tmp) {  
989
    __retres2 = 0;  
990
    goto return_label;  
991
  } else {  
992
  
993
  }  
994
  __retres2 = 1;  
995
  return_label: /* CIL Label */   
996
  return (__retres2);  
997
}  
998
}  
999
void start_simulation(void)   
1000
{ int kernel_st ;  
1001
  int tmp ;  
1002
  int tmp___0 ;  
1003
  
1004
  {  
1005
  {  
1006
  kernel_st = 0;  
1007
  update_channels();  
1008
  init_threads();  
1009
  fire_delta_events();  
1010
  activate_threads();  
1011
  reset_delta_events();  
1012
  }  
1013
  {  
1014
  while (1) {  
1015
    while_9_continue: /* CIL Label */ ;  
1016
    {  
1017
    kernel_st = 1;  
1018
    eval();  
1019
    }  
1020
    {  
1021
    kernel_st = 2;  
1022
    update_channels();  
1023
    }  
1024
    {  
1025
    kernel_st = 3;  
1026
    fire_delta_events();  
1027
    activate_threads();  
1028
    reset_delta_events();  
1029
    }  
1030
    {  
1031
    tmp = exists_runnable_thread();  
1032
    }  
1033
    if (tmp == 0) {  
1034
      {  
1035
      kernel_st = 4;  
1036
      fire_time_events();  
1037
      activate_threads();  
1038
      reset_time_events();  
1039
      }  
1040
    } else {  
1041
  
1042
    }  
1043
    {  
1044
    tmp___0 = stop_simulation();  
1045
    }  
1046
    if (tmp___0) {  
1047
      goto while_9_break;  
1048
    } else {  
1049
  
1050
    }  
1051
  }  
1052
  while_9_break: /* CIL Label */ ;  
1053
  }  
1054
  
1055
  return;  
1056
}  
1057
}  
1058
int main(void)   
1059
{ int __retres1 ;  
1060
  
1061
  {  
1062
  {  
1063
  init_model();  
1064
  start_simulation();  
1065
  }  
1066
  __retres1 = 0;  
1067
  return (__retres1);  
1068
}  
1069
}  
DateTimeLevelComponentMessage
2025-08-2817:02:33:080INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2025-08-2817:02:33:155INFOCPAchecker.runCPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started
2025-08-2817:02:33:173INFOCPAchecker.parseParsing CFA from file(s) "Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/transmitter.06_false-unreach-call_false-termination.cil/transmitter.06_false-unreach-call_false-termination.cil.c"
2025-08-2817:02:34:578INFOCoreComponentsFactory.createAlgorithmUsing Restarting Algorithm
2025-08-2817:02:34:598WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.arg.lateMerge
counterexample.export.exportWitness
2025-08-2817:02:34:598INFOCPAchecker.runAlgorithmStarting analysis ...
2025-08-2817:02:34:612INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ...
2025-08-2817:02:34:684INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
ResourceLimitChecker.fromConfiguration
Using the following resource limits: Thread CPU-time limit of 300s
2025-08-2817:02:35:023INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2817:02:35:476INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2817:02:35:489WARNINGCPAs.retrieveCPAOrFailWarning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA)
2025-08-2817:02:35:493INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ...
2025-08-2817:02:35:500INFONestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'.
2025-08-2817:02:35:529WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2817:02:35:533INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2817:02:35:700INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2817:02:35:767WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2817:02:35:808INFORestartAlgorithm.runStarting analysis 1 ...
2025-08-2817:02:35:809INFOAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.run0
Starting termination algorithm.
2025-08-2817:17:31:709WARNINGForceTerminationOnShutdown$1.shutdownRequestedShutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination.
2025-08-2817:17:31:721WARNINGShutdownNotifier.shutdownIfNecessaryWarning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.)
Statistics NameStatistics ValueAdditional Value
Restart Algorithm statistics
Number of algorithms provided 2
Number of algorithms used 1
Last algorithm used /cpachecker/config/components/combinations-parallel-termination.properties
Total time for algorithm 1 897.107s
PredicateCPA statistics
Number of abstractions 26 0% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 23 88%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 3 12%
Times precision was empty 15 58%
Times precision was {false} 0 0%
Times result was cached 3 12%
Times cartesian abs was used 0 0%
Times boolean abs was used 8 31%
Times result was 'false' 1 4%
Number of strengthen sat checks 0
Number of coverage checks 6203
BDD entailment checks 16
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 465
Avg ABE block size 247.42 sum: 6433, count: 26, min: 0, max: 465
Number of predicates discovered 28
Number of abstraction locations 2
Max number of predicates per location 28
Avg number of predicates per location 27
Total predicates per abstraction 300
Max number of predicates per abstraction 28
Avg number of predicates per abstraction 37.50
Number of irrelevant predicates 3 1%
Number of preds handled by boolean abs 216 72%
Total number of models for allsat 3110
Max number of models for allsat 1426
Avg number of models for allsat 388.75
Time for post operator 0.880s
Time for path formula creation 0.862s
Time for strengthen operator 0.035s
Time for prec operator 4.781s
Time for abstraction 4.733s Max: 2.180s, Count: 26
Boolean abstraction 4.582s
Solving time 0.053s Max: 0.010s
Model enumeration time 4.514s
Time for BDD construction 0.197s Max: 0.004s
Time for merge operator 0.092s
Time for coverage checks 0.009s
Time for BDD entailment checks 0.006s
Total time for SMT solver (w/o itp) 4.567s
Number of path formula cache hits 9659 43%
Inside post operator
Inside path formula creation
Time for path formula computation 0.831s
Total number of created targets for pointer analysis 0
Number of BDD nodes 128040
Size of BDD node table 466043
Size of BDD cache 46619
Size of BDD node cleanup queue 2.09 sum: 3030, count: 1449, min: 0, max: 1694
Time for BDD node cleanup 0.000s
Time for BDD garbage collection 0.000s in 0 runs
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
AutomatonAnalysis (NonTerminationLabelAutomaton) statistics
Number of states 1
Total time for successor computation 0.088s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 20587, count: 20597, min: 0, max: 1 [0 x 10, 1 x 20587]
Number of states with assumption transitions 0
AutomatonAnalysis (TerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.028s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 20587, count: 20587, min: 1, max: 1 [1 x 20587]
Number of states with assumption transitions 0
Termination Algorithm statistics
Total time 895.911s
Time for recursion analysis 0.000s
Number of analysed loops 1 50%
Total time for loop analysis 895.903s
Avg time per loop analysis 895.903s
Max time per loop analysis 895.903s
Number of safety analysis runs 1
Avg safety analysis run per loop 1.00
Max safety analysis run per loop 1 for loops [N743]
Total time for safety analysis 7.688s
Avg time per safety analysis run 7.688s
Max time per safety analysis run 7.688s
Number of analysed lassos 0
Avg number of lassos per loop 0.00
Max number of lassos per loop 0 for loops
Avg number of lassos per iteration 0.00
Max number of lassos per iteration 0
Total time for lassos analysis 888.188s
Avg time per iteration 888.188s
Max time per iteration 888.188s
Time for lassos construction 888.188s
Avg time for lasso construction per iteration 888.188s
Max time for lasso construction per iteration 888.188s
Time for stem and loop construction 0.148s
Avg time for stem and loop construction per iteration 0.148s
Max time for stem and loop construction per iteration 0.148s
Time for lassos creation 888.038s
Avg time for lassos creation per iteration 888.038s
Max time for lassos creation per iteration 888.038s
Total time for non-termination analysis 0.000s
Avg time for non-termination analysis per lasso 0.000s
Max time for non-termination analysis per lasso 0.000s
Total time for termination analysis 0.000s
Avg time for termination analysis per lasso 0.000s
Max time for termination analysis per lasso 0.000s
Total number of termination arguments 0
Avg termination arguments per loop 0.00
Max termination arguments per loop 0 for loops
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Termination Algorithm statistics
Total time 895.911s
Time for recursion analysis 0.000s
Number of analysed loops 1 50%
Total time for loop analysis 895.903s
Avg time per loop analysis 895.903s
Max time per loop analysis 895.903s
Number of safety analysis runs 1
Avg safety analysis run per loop 1.00
Max safety analysis run per loop 1 for loops [N743]
Total time for safety analysis 7.688s
Avg time per safety analysis run 7.688s
Max time per safety analysis run 7.688s
Number of analysed lassos 0
Avg number of lassos per loop 0.00
Max number of lassos per loop 0 for loops
Avg number of lassos per iteration 0.00
Max number of lassos per iteration 0
Total time for lassos analysis 888.188s
Avg time per iteration 888.188s
Max time per iteration 888.188s
Time for lassos construction 888.188s
Avg time for lasso construction per iteration 888.188s
Max time for lasso construction per iteration 888.188s
Time for stem and loop construction 0.148s
Avg time for stem and loop construction per iteration 0.148s
Max time for stem and loop construction per iteration 0.148s
Time for lassos creation 888.038s
Avg time for lassos creation per iteration 888.038s
Max time for lassos creation per iteration 888.038s
Total time for non-termination analysis 0.000s
Avg time for non-termination analysis per lasso 0.000s
Max time for non-termination analysis per lasso 0.000s
Total time for termination analysis 0.000s
Avg time for termination analysis per lasso 0.000s
Max time for termination analysis per lasso 0.000s
Total number of termination arguments 0
Avg termination arguments per loop 0.00
Max termination arguments per loop 0 for loops
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Code Coverage
Function coverage 1.000
Visited lines 458
Total lines 460
Line coverage 0.996
Visited conditions 212
Total conditions 212
Condition coverage 1.000
CPAchecker general statistics
Number of program locations 740
Number of CFA edges (per node) 854 count: 740, min: 0, max: 6, avg: 1.15
Number of relevant variables 70
Number of functions 29
Number of loops (and loop nodes) 2 sum: 98, min: 22, max: 76, avg: 49.00
Size of reached set 9184
Number of reached locations 616 83%
Avg states per location 14
Max states per location 49 at node N595
Number of reached functions 29 100%
Number of partitions 616
Avg size of partitions 14
Max size of partitions 49 with key N595
Number of target states 1
Size of final wait list 9
Time for analysis setup 1.425s
Time for loading CPAs 0.015s
Time for loading parser 0.216s
Time for CFA construction 1.153s
Time for parsing file(s) 0.302s
Time for AST to CFA 0.381s
Time for CFA sanity check 0.094s
Time for post-processing 0.243s
Time for loop structure 0.013s
Time for AST structure 0.000s
Time for CFA export 0.666s
Time for function pointers resolving 0.008s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.126s
Time for collecting variables 0.082s
Time for solving dependencies 0.003s
Time for building hierarchy 0.000s
Time for building classification 0.036s
Time for exporting data 0.005s
Time for Analysis 897.110s
CPU time for analysis 947.970s
Total time for CPAchecker 898.552s
Total CPU time for CPAchecker 950.420s
Time for statistics 0.269s
Time for Garbage Collector 8.176s in 5024 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 1646MB ( 1570 MiB) max; 704MB ( 672 MiB) avg; 1993MB ( 1900 MiB) peak
Used non-heap memory 60MB ( 57 MiB) max; 59MB ( 57 MiB) avg; 61MB ( 58 MiB) peak
Used in PS Old Gen pool 1135MB ( 1082 MiB) max; 571MB ( 545 MiB) avg; 1135MB ( 1082 MiB) peak
Allocated heap memory 3349MB ( 3194 MiB) max; 1794MB ( 1711 MiB) avg
Allocated non-heap memory 63MB ( 60 MiB) max; 63MB ( 60 MiB) avg
Total process virtual memory 14915MB ( 14224 MiB) max; 14896MB ( 14206 MiB) avg
#Configuration NameConfiguration Value
1analysis.algorithm.termination true
2analysis.machineModel Linux64
3analysis.name terminationAnalysis
4analysis.programNames Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/transmitter.06_false-unreach-call_false-termination.cil/transmitter.06_false-unreach-call_false-termination.cil.c
5analysis.restartAfterUnknown true
6counterexample.export.exportWitness false
7cpa.arg.lateMerge prevent
8language C
9log.level INFO
10parser.usePreprocessor true
11restartAlgorithm.configFiles components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive
12specification
13statistics.print true
14termination.config terminationAnalysis.properties

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}